i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), T:Type, ks:(Knd List), upd:update-spec(ds; da),
a:((k:{k:Knd| (k  ks)} decl-state(ds)ma-valtype(da; k)T)).
((fpf-dom(id-deq; mkid{ecl:ut2}; ds)))
 normal-type{i:l}
 normal-type(T)
 normal-ds{i:l}
 normal-ds(ds)
 normal-da{i:l}
 normal-da(da)
 l_all(ks; Knd; k.((isrcv(k))  (i = destination(lnk(k))  Id)))
 update-spec-decl(upd; ds)
 R-realizes{i:l}
 R-realizes(ecl-machine2(i; ds; da; mkid{ecl:ut2}; T; ks; a; upd);
 R-realizes(es.l_all(update-spec-vars(upd);
 R-realizes(es.l_all(Id;
 R-realizes(es.l_all(z.(es-decls(es;i;fpf-join(id-deq; ds; fpf-single(mkid{ecl:ut2}; T));da)
 R-realizes(es.l_all( (subtype_rel(es-vartype(es; i; z); fpf-ap(ds; id-deq; z))
 R-realizes(es.l_all( c ((bor((null(ks)); es-isconst(es; i; z)))
 R-realizes(es.l_all( c  alle-at(es;
 R-realizes(es.l_all( c  alle-at(i;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-after(es; z; e')
 R-realizes(es.l_all( c  alle-at(e.e'e.=
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}(es;ks;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}(k,s,v,z'. list_accum
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((z',nf.let n,f = nf
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((in
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((if a
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((if (n
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((if ,k
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((if ,s
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((if ,v
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((if ,s(mkid{ecl:ut2}))
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((then f(s,v)
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((else z'
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fi ;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((z';
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap(upd;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap(product-deq
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap((Knd;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap((Id;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap((Kind-deq;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap((id-deq);
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap(<k, z>;
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((fpf-cap([]));es-when
 R-realizes(es.l_all( c  alle-at(e.e'e.es-trans-state-from{i:l}((es; z; e);e;e')
 R-realizes(es.l_all( c  alle-at(e.e'e. fpf-ap(ds; id-deq; z))))))) 

latex

Definitions

prop{i:l}, ff, tt, top, x,y. t(x;y), x. t(x), t.2, t.1, t  T, x:A. B(x), fpf-cap(f; eq; x; z), if b then t else f fi , P  Q, mkid{$x:ut2}, decl-state(ds), Id, P  Q, es-le(es; e; e'), x:A. B(x), e'e.P(e'), alle-at(es; i; e.P(e)), A c B, (x  l), False, A  B, A, Knd, ma-valtype(da; k), P  Q, P  Q, Unit, x(s), x(s1,s2), , update-spec(ds; da), update-spec-decl(upd; ds), guard(T), , , ecl-machine2(i; ds; da; x; T; ks; a; upd)

Lemmas

fpf-cap-join-subtype, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, eqtt to assert, bool wf, fpf-dom wf, eqof eq btrue, fpf-cap-single, fpf-trivial-subtype-top, id-deq wf, fpf-join-cap-sq, fpf-sub weakening, deq wf, subtype rel self, fpf-sub-join-left2, subtype-fpf-cap-top, top wf, fpf-single wf, fpf-join wf, fpf-cap wf, subtype rel dep function, fpf-ap wf, list accum wf, es-vartype wf, es-le-loc, es-after wf, es-locl wf, IdLnk wf, select wf, length wf1, es-when wf, es-isrcv wf, es-loc wf, es-trans-state-from wf, es-decls-iff